Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,from(s(X)))
2:		2ndspos(0,Z)	→ rnil
3:		2ndspos(s(N),cons(X,cons(Y,Z)))	→ rcons(posrecip(Y),2ndsneg(N,Z))
4:		2ndsneg(0,Z)	→ rnil
5:		2ndsneg(s(N),cons(X,cons(Y,Z)))	→ rcons(negrecip(Y),2ndspos(N,Z))
6:		pi(X)	→ 2ndspos(X,from(0))
7:		plus(0,Y)	→ Y
8:		plus(s(X),Y)	→ s(plus(X,Y))
9:		times(0,Y)	→ 0
10:		times(s(X),Y)	→ plus(Y,times(X,Y))
11:		square(X)	→ times(X,X)

There are 9 dependency pairs:


12:		FROM(X)	→ FROM(s(X))
13:		2ndspos#(s(N),cons(X,cons(Y,Z)))	→ 2ndsneg#(N,Z)
14:		2ndsneg#(s(N),cons(X,cons(Y,Z)))	→ 2ndspos#(N,Z)
15:		PI(X)	→ 2ndspos#(X,from(0))
16:		PI(X)	→ FROM(0)
17:		PLUS(s(X),Y)	→ PLUS(X,Y)
18:		TIMES(s(X),Y)	→ PLUS(Y,times(X,Y))
19:		TIMES(s(X),Y)	→ TIMES(X,Y)
20:		SQUARE(X)	→ TIMES(X,X)

The approximated dependency graph contains 4 SCCs: {13,14}, {12}, {17} and {19}.

Consider the SCC {13,14}. There are no usable rules. By taking the AF π with π(2ndsneg#) = π(2ndspos#) = 1 together with the lexicographic path order with empty precedence, the rules in {13,14} are strictly decreasing.

Consider the SCC {12}. There are no usable rules. The constraints could not be solved.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {19}. There are no usable rules. By taking the AF π with π(TIMES) = 1 together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Tyrolean Termination Tool (0.05 seconds) --- May 4, 2006